% This is "sig-alternate.tex" V2.0 May 2012
% This file should be compiled with V2.5 of "sig-alternate.cls" May 2012
%
% This example file demonstrates the use of the 'sig-alternate.cls'
% V2.5 LaTeX2e document class file. It is for those submitting
% articles to ACM Conference Proceedings WHO DO NOT WISH TO
% STRICTLY ADHERE TO THE SIGS (PUBS-BOARD-ENDORSED) STYLE.
% The 'sig-alternate.cls' file will produce a similar-looking,
% albeit, 'tighter' paper resulting in, invariably, fewer pages.
%
% ----------------------------------------------------------------------------------------------------------------
% This .tex file (and associated .cls V2.5) produces:
%       1) The Permission Statement
%       2) The Conference (location) Info information
%       3) The Copyright Line with ACM data
%       4) NO page numbers
%
% as against the acm_proc_article-sp.cls file which
% DOES NOT produce 1) thru' 3) above.
%
% Using 'sig-alternate.cls' you have control, however, from within
% the source .tex file, over both the CopyrightYear
% (defaulted to 200X) and the ACM Copyright Data
% (defaulted to X-XXXXX-XX-X/XX/XX).
% e.g.
% \CopyrightYear{2007} will cause 2007 to appear in the copyright line.
% \crdata{0-12345-67-8/90/12} will cause 0-12345-67-8/90/12 to appear in the copyright line.
%
% ---------------------------------------------------------------------------------------------------------------
% This .tex source is an example which *does* use
% the .bib file (from which the .bbl file % is produced).
% REMEMBER HOWEVER: After having produced the .bbl file,
% and prior to final submission, you *NEED* to 'insert'
% your .bbl file into your source .tex file so as to provide
% ONE 'self-contained' source file.
%
% ================= IF YOU HAVE QUESTIONS =======================
% Questions regarding the SIGS styles, SIGS policies and
% procedures, Conferences etc. should be sent to
% Adrienne Griscti (griscti@acm.org)
%
% Technical questions _only_ to
% Gerald Murray (murray@hq.acm.org)
% ===============================================================
%
% For tracking purposes - this is V2.0 - May 2012

\documentclass{sig-alternate}

\usepackage[utf8]{inputenc}
\input{DeclareUnicodeCharacter}
\usepackage{color}
\definecolor{shadecolor}{rgb}{.9,.9,1} 
\usepackage{url}

\usepackage{tikz}
\usetikzlibrary{matrix,arrows}
%\usepackage{pgfplots}
%\usetikzlibrary{plotmarks}
%\usetikzlibrary{positioning}
%\usetikzlibrary{shapes,shadows,arrows}
\usetikzlibrary{calc}
%%\pgfplotsset{compat=1.3}
%\pgfdeclarelayer{background}
%\pgfdeclarelayer{foreground}
%\pgfsetlayers{background,main,foreground}

\newcommand{\LPBs}{\mathit{LPBs}}
\newcommand{\sd}[1]{\colorbox{shadecolor}{#1}}
\newcommand{\ld}[1]{\raisebox{-1ex}[0cm][0cm]{\sd{#1}}}
\newcommand{\ud}[1]{\raisebox{1ex}[0cm][0cm]{\sd{#1}}}
\newcommand{\ub}[1]{\raisebox{1ex}[0cm][0cm]{#1}}
\newcommand{\repeatlabel}[1]{\label{#1}}
\newcommand{\defining}[1]{\textbf{#1}}
\newcommand{\bool}{\mathit{Bool}}
\newcommand{\real}{\mathbb{R}}
\newcommand{\false}{\mathit{false}}
\newcommand{\true}{\mathit{true}}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\integ}{\mathbb{Z}}
\newcommand{\onetom}{{[1..m]}}
\newcommand{\onetol}{{[1..l]}} 
\newcommand{\zerotol}{{[0..l]}}   
\newcommand{\iso}{\mathfrak{I}^\leq}
\newcommand{\isop}{\mathfrak{I}^=}
\newcommand{\ineq}{\mathit{Ineq}^\leq}
\newcommand{\ineqp}{\mathit{Ineqp}^=}
\newcommand{\mono}{\mathfrak{M}^\leq}
\newcommand{\monop}{\mathfrak{M}^=}
\newcommand{\coeffSum}[2]{\sum_{i=#1}^{#2}a_ix_i}
\newcommand{\coeffSumPrime}[2]{\sum_{i=#1}^{#2}a'_ix_i}
\newcommand{\ms}[1]{\{\hspace{-0.2em}[#1]\hspace{-0.2em}\}}
\newcommand{\OP}{\mathit{OP}}
\newcommand{\Cut}[3]{\mathit{S}(#1,#2,#3)}
\newcommand{\CutT}[2]{\mathit{S}(\cdot,#1,#2)}
\newcommand{\mint}{s}
\newcommand{\maxt}{b}
\newcommand{\threshold}[2]{(#1,#2]}
\newcommand{\LPBT}[2]{}%\mathit{I}(#1,#2)\equiv}

%For pseudocode
\newcommand{\uc}{\mathit{uc}}
\newcommand{\lc}{\mathit{lc}}
\newcommand{\parent}{\mathit{parent}}
\newcommand{\col}{\mathit{col}}
\newcommand{\pat}{\mathit{path}}
\newcommand{\MU}{\mathit{MU}}
\newcommand{\ML}{\mathit{ML}}
\newcommand{\NU}{\mathit{NU}}
\newcommand{\NL}{\mathit{NL}}
\newcommand{\MUs}{\mathit{MUs}}
\newcommand{\MLb}{\mathit{MLb}}
\newcommand{\NUb}{\mathit{NUb}}
\newcommand{\NLs}{\mathit{NLs}}
\newcommand{\MUU}{\mathit{MUU}}
\newcommand{\MLU}{\mathit{MLU}}
\newcommand{\NUU}{\mathit{NUU}}
\newcommand{\NLU}{\mathit{NLU}}
\newcommand{\MUL}{\mathit{MUL}}
\newcommand{\MLL}{\mathit{MLL}}
\newcommand{\NUL}{\mathit{NUL}}
\newcommand{\NLL}{\mathit{NLL}}
\newcommand{\jump}{\mathit{jump}}
\newcommand{\repair}{\mathrm{repair}}


\newtheorem{theorem}{Theorem}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{example}[theorem]{Example}
\newtheorem{corollary}[theorem]{Corollary}


\begin{document}
%
% --- Author Metadata here ---
%\CopyrightYear{2007} % Allows default copyright year (20XX) to be over-ridden - IF NEED BE.
%\crdata{0-12345-67-8/90/01}  % Allows default copyright data (0-89791-88-6/97/05) to be over-ridden - IF NEED BE.
% --- End of Author Metadata ---

\title{Implementation of two Algorithms for the Threshold Synthesis Algorithms}
%\subtitle{[Extended Abstract]
%\titlenote{A full version of this paper is available as
%\textit{Author's Guide to Preparing ACM SIG Proceedings Using
%\LaTeX$2_\epsilon$\ and BibTeX} at
%\texttt{www.acm.org/eaddress.htm}}}
%
% You need the command \numberofauthors to handle the 'placement
% and alignment' of the authors beneath the title.
%
% For aesthetic reasons, we recommend 'three authors at a time'
% i.e. three 'name/affiliation blocks' be placed beneath the title.
%
% NOTE: You are NOT restricted in how many 'rows' of
% "name/affiliations" may appear. We just ask that you restrict
% the number of 'columns' to three.
%
% Because of the available 'opening page real-estate'
% we ask you to refrain from putting more than six authors
% (two rows with three columns) beneath the article title.
% More than six makes the first-page appear very cluttered indeed.
%
% Use the \alignauthor commands to handle the names
% and affiliations for an 'aesthetic maximum' of six authors.
% Add names, affiliations, addresses for
% the seventh etc. author(s) as the argument for the
% \additionalauthors command.
% These 'additional authors' will be output/set for you
% without further effort on your part as the last section in
% the body of your article BEFORE References or any Appendices.

\numberofauthors{3} %  in this sample file, there are a *total*
% of EIGHT authors. SIX appear on the 'first-page' (for formatting
% reasons) and the remaining two appear in the \additionalauthors section.
%
% You can go ahead and credit any number of authors here,
% e.g. one 'row of three' or two rows (consisting of one row of three
% and a second row of one, two or three).
%
% The command \alignauthor (no curly braces needed) should
% precede each author name, affiliation/snail-mail address and
% e-mail address. Additionally, tag each line of
% affiliation/address with \affaddr, and tag the
% e-mail address with \email.
%
%\author{
%\alignauthor
%Christian Schilling\\
%       \affaddr{Institut für Informatik}\\
%       \affaddr{Universität Freiburg}\\
%       \affaddr{Germany}\\
%       \email{schillic@informatik.uni-freiburg.de}
%\alignauthor
%Jan-Georg Smaus\\
%       \affaddr{IRIT}
%       \affaddr{Université de Toulouse}\\
%       \affaddr{France}\\
%       \email{smaus@irit.fr}
%\alignauthor
%Fabian Wenzelmann\\
%       \affaddr{Institut für Informatik}\\
%       \affaddr{Universität Freiburg}\\
%       \affaddr{Germany}\\
%       \email{wenzelmf@informatik.uni-freiburg.de}
%}
%Authors must remain anonymous for submission


\maketitle

%\vspace*{-5cm}


% A category with the (minimum) three required fields
\category{G.2.1}{Discrete Mathematics}{Combinatorics}[Combinatorial
algorithms]
\category{G.1.6}{Numerical analysis}{Optimization}[Integer
programming, linear programming]
\category{E.1}{Data structures}{Graphs and networks, trees}
\category{G.1.0}{Numerical analysis}{General}[Interval arithmetic]
%\category{G.1.3}{Numerical analysis}{Numerical linear algebra}[Linear systems]


\terms{Algorithms, experimentation, theory}

\keywords{Boolean functions, threshold logic, linearly separable functions}

%\input{macros}

\bibliographystyle{plain}
%\pagestyle{plain}
\pagestyle{empty}%TR230


\begin{abstract}
A \emph{linear pseudo-Boolean constraint} (LPB) is an expression of
the form $$a_1\cdot \ell_1+\ldots+a_m\cdot \ell_m\geq d,$$ where each
$\ell_i$ is a \emph{literal} (it assumes the value 1 or 0 depending on
whether a propositional variable $x_i$ is true or false) and
$a_1,\ldots,a_m,d$ are natural numbers. An LPB represents a Boolean
function, and those Boolean functions that can be represented by
exactly one LPB are called \emph{threshold functions}.  The problem of
finding an LPB representation of a Boolean function if possible is
called \emph{threshold recognition problem} or \emph{threshold
  synthesis problem}.  The problem has an $O(m^7t^5)$
algorithm using linear programming, where $m$ is the dimension and $t$
the number of terms in the DNF input. There is also an entirely 
combinatorial procedure, which works by decomposing the DNF and ``counting'' the
variable occurrences in it. We have implemented
both algorithms and report here on the
experiments. 
We were able to solve problems of up to
%TODO
variables. 
\end{abstract}


\section{Introduction}\label{intro-sec}
A \emph{linear pseudo-Boolean constraint} (LPB)
\cite{CraHam11,%AloRamMarSak02,Bar93,
ChaKue03,%seems important because at least they actually use the name "LPB"
DixGin-KER00%seems rich in applications. AI + operations research
%,Dix04,
%FraHer03,FraHer06
} 
is an expression of the form
$a_1\ell_1+\ldots+a_m\ell_m\geq d$. Here each $\ell_i$ is a \emph{literal} of
the form $x_i$ or $\bar{x}_i\equiv1-x_i$, i.e.~$x_i$ becomes 0 if $x_i$
is false and 1 if $x_i$ is true, and vice versa for $\bar{x}_i$. 
Moreover, $a_1,\ldots,a_m,d$ are natural numbers. 

An LPB can be used to represent a Boolean\footnote{Whenever we say ``function''
  we mean ``Boolean function''.}
function; e.g.~$x_1+\bar{x}_2+x_3\geq3$ represents the 
same  function as the propositional formula 
$x_1\land¬ x_2\land x_3$% 
%(we identify propositional formulae with  functions)
. It has been observed that a 
function can be often represented more compactly as a set of LPBs than
as a \emph{conjunctive} or \emph{disjunctive} normal form (CNF or DNF) 
\cite{ChaKue03,DixGin-KER00}. 
E.g.~the LPB $2x_1+\bar{x}_2+x_3+x_4\geq2$ corresponds to the DNF 
$x_1\lor(¬ x_2\land x_3)\lor(¬ x_2\land x_4)\lor(x_3\land x_4)$. 

Functions that can be represented by a single LPB are called
\emph{threshold functions} \cite{She69}. 
The interest in threshold functions comes from various applications
in artificial intelligence \cite{BarBoc93}, 
electronic design automation \cite{ChaKue03}, 
game theory \cite{Bol11}, and several others 
(see \cite{GowVru08} and references therein). 
%the
%pigeonhole problem \cite{DixGin-KER00}, and gate level netlists
%\cite{FraHer03}.

The problem of finding the LPB for a threshold function given as DNF
is called \emph{threshold synthesis problem}. The problem is known to have an
$O(m^7t^5)$ algorithm using linear programming, where $m$ is the
dimension and $t$ the number of terms in the DNF \cite{CraHam11}.  
In this paper, we report on an implementation of this
solution to the problem. Moreover, we report on an implementation of a
``combinatorial'' algorithm for the problem first proposed by Coates
\emph{et al.}  \cite{CoaLew61,CoaKirLew62} and rediscovered later by
Smaus \cite{Sma-CPAIOR07}. It works
by decomposing the DNF and ``counting'' its variable occurrences 
in an appropriate way.
%TODO: Depending on the results of the experiments, let's be more
%specific here. 

The threshold recognition problem has attracted interest also in the
VLSI community. Recently, a method for solving the problem has been
presented at this very venue \cite{PalGopTra10}. In experiments, the
authors were able to identify 36 10-variable threshold functions 
among 10000 candidate functions --- unfortunately, nobody knows how
many of those 10000 functions actually were threshold functions, so
that the statement says little about the real power of their method. 
The methods we present here were tried on XX functions of up to XX
variables, known to be threshold, and could identify all of them. 
%XX \% of them 
%TODO

%TODO: reconsider
This paper is organised as follows. 
We continue with some preliminaries. Sec.~\ref{lp-sec} describes the
linear programming algorithm, Sec.~\ref{encoding-sec} the
combinatorial procedure, 
Sec.~\ref{random-sec} the generation of our benchmarks, 
Sec.~\ref{impl-sec} the implementation, and Sec.~\ref{concl-sec}
concludes 
and discusses future work. 

\section{Preliminaries}\label{prelim-sec}
%We assume the reader to be familiar with the basic notions of
%propositional logic. 

An \defining{$m$-dimensional Boolean function} $f$ is a function 
$\bool^m\to\bool$. 

We follow \cite{ChaKue03}.
%I briefly checked my notes. This seems to be true.  
A \defining{linear pseudo-Boolean constraint} (LPB)
is an inequality of the form
\begin{equation}\label{LPB-eq}
a_1\ell_1+\ldots+a_m\ell_m\geq d
\qquad a_i\in\nat, d\in\integ, \ell_i\in\{x_i,\bar{x}_i\}
\end{equation}
where $\bar{x}_i\equiv1-x_i$. 
We identify 0 with $\false$ and 1 with $\true$. 
We call the $a_i$ \defining{coefficients} and $d$ the
\defining{threshold} (\defining{threshold}). 

%Note that if $d\leq0$, then the LPB is a
%tautology. The reason for allowing for negative $d$ will become
%apparent in Subsec.~\ref{decomposition-subsec}.
%An LPB is in \defining{normal form} if $d\geq a_1\geq\ldots\geq a_m$ \cite{Bar93}.  
%Careful: we should not rule out tautologies a-priori, and then
%$d<a_1$, even $d<0$, can have a justification. 

A \defining{DNF} is a 
%propositional 
formula of the form $c_1\lor\ldots\lor c_n$
where each \defining{clause} $c_j$ is a conjunction of literals. 
Formally,  a DNF is a set of sets of literals,
i.e., the order of clauses and the order of
literals within a clause are insignificant.
For DNFs, we
assume without loss of generality that no clause %'s literal set 
is a subset of another clause %'s literal set 
(%it is easy to see that 
the latter clause would be redundant since it is \emph{absorbed}).
We call a DNF \emph{prime irredundant} if every clause is a prime implicant, i.e.,
if for clause $c_1$ there is no clause $c_2 \neq c_1$ such that $c_1 \lor c_2 = c_2$.
Any Boolean function can be represented by a DNF \cite{Weg87-nohtml}.%TR230

It is easy to see that an LPB can only represent \emph{monotone}
functions, i.e., functions represented by a DNF where each variable
occurs in only one polarity. Hence any DNF containing a variable in
different polarities is immediately uninteresting for us. 
Without loss of generality, we assume that this polarity
is positive. 


Variables 
$x$ and $y$ are \defining{symmetric} in $\phi$
 if $\phi$ is equivalent to
the formula obtained by exchanging $x$ and $y$.  
A set of variables $Y$ is \defining{symmetric} in $\phi$ 
if each pair in $Y$ is symmetric in $\phi$. 

%TODO: Put back in if there is enough space. 
%We consider two ways of measuring how much increase there is from the
%smallest to the biggest coefficient in an LPB.
%%
%The first is the \textbf{symmetry quotient} defined as 
%$\frac{\#\{a_i \mid a_i=a_{i-1}\}}{m-1}$, i.e., the number of repetitions of
%identical coefficients, 
%divided by the maximal number of repetitions there could be (every
%coefficient is identical to the previous one). 
%%
%The other is $(\frac{a_1}{a_m})^{\frac{1}{m-1}}$, i.e., the average
%ratio between 2 subsequent coefficients, which we call the
%\textbf{excentricity} of the LPB. 
 

\section{The Linear Programming Algorithm}\label{lp-sec}
We shortly summarise the solution via linear programming, 
established by Peled \& Simeone \cite{PeledSimeone85,CraHam11}. 

For some DNFs, it is possible to establish a complete order $\succeq$ on the
variables which, intuitively speaking, has the following meaning:
$x_i\succeq x_j$ iff starting from any given input tuple $X^* \in \bool^m$,
setting $x_i^*$ to true is more likely to make the DNF true than
setting $x_j^*$ true. The functions represented by such a DNF are called 
\emph{regular}.

The order is based
on \emph{occurrence patterns} %\cite{Sma-CPAIOR07} 
(the \emph{Winder
  matrix} \cite{CraHam11,winder62}) and can be computed in time linear
in $|\phi|$. For space reasons, we omit the actual definition of $\succeq$ here. 
We write $x_i\simeq x_k$ if $x_i\succeq x_k$ and $x_k\succeq x_i$. 

We will need the $\succeq$ order again in the next section.

%Note that if $\coeffSum{1}{m}\geq d$ is an LPB representing the DNF
%$\phi$ and $a_i=a_k$, then $x_i,x_k$ are symmetric in $\phi$; but $a_i\neq a_k$
%does not imply that $x_i,x_k$ are not symmetric. 
%For example, $x_1\lor x_2$ can be represented by $2x_1+x_2\geq1$ or 
%$x_1+x_2\geq1$. 

%Computing the set of occurrence patterns for all variables in $\phi$ can
%be done in time linear in $|\phi|$. In fact, the number of elements of all
%occurrence patterns is exactly the number of literals in $\phi$. 
%Thus sorting the variables w.r.t.~the occurrence patterns can be done
%in time polynomial in $|\phi|$. 


The algorithm first tests the input DNF for the
regularity property. The property is weaker than
the threshold property, and so if a DNF is not regular, then it is not
convertible and we must give up.



Provided the DNF is regular, 
we make use of the \emph{minimal true points} of the DNF, 
i.e.~the true tuples where we cannot set any 1-value to 0 without making the point false.
We also use the \emph{maximal false points} defined analogously.
Note that these together characterise the DNF uniquely.
In general, no polynomial algorithm is known to find these points
(which is no surprise since the general task is NP-complete \cite{PeledSimeone85}),
but for the special case that the input DNF is prime irredundant this is possible.
The reason is that the true points can be read directly from the clauses.
It is for this reason that we require the 
input DNF to be in prime irredundant form.

Having these, there exists a polynomial time procedure to find the maximal false points.
Then we can formulate the following linear program where the minimal true points are $x^1,\dots,x^k$ and the 
maximal false points are $y^1,\dots,y^l$:
%\marginpar{Habe dies direkter und mehr in Analogie zum Rest des Papers
%formuliert, zB diese ``+1'' Sache ist weg. Bitte nur rueckgaengig
%machen, wenn das wirklich grob falsch sein sollte.}
\begin{alignat*}{8}
	\sum_{i=1}^m a_i x_i^j &\quad& \geq &\quad&& d &\quad& (1 \leq j \leq k) \\
	\sum_{i=1}^m a_i y_i^j && < &&& d && (1 \leq j \leq l) \\
	a_i && \geq &&& 0 && (1 \leq i \leq m)
\end{alignat*}
Note that the weights $a_i$ are the variables in the LP formulation and the threshold is $d$.
Finally, the linear program is passed to an LP solver.
The reason for the complexity blow-up ($O(m^7t^5)$ where $m$ is the dimension and $t$ the number of terms in the DNF)
is mainly due to the linear programming.
The other parts run in $O(m^2t)$, so the whole procedure gains from future improvements of linear programming.
It should be mentioned that for most inputs the well-known simplex method for solving linear programs runs in linear time.
 


\section{Combinatorial Algorithm}\label{encoding-sec}
%TODO: kürzen
In this section we present a combinatorial algorithm for the threshold
synthesis problem first presented by Coates \emph{et al.}
\cite{CoaLew61,CoaKirLew62} and rediscovered later by Smaus
\cite{Sma-CPAIOR07}. 
The algorithm is divided into a basic algorithm (Part I
\cite{CoaLew61}) which is correct but incomplete, and a backtracking
procedure to obtain completeness Part II and II \cite{CoaLew61}). 
For space reasons, we only describe Part I in detail here, but our
implementation covers all parts. 

%\subsection{Determining the Order of Coefficients}\label{coefficient-order-subsec}
Consider again the order $\succeq$ of the variables: it must be respected by
any LPB (if there is one!)  representing $\phi$, i.e., $x_i\succeq x_k$ implies
$a_i\geq a_k$. Note that $x_i\succ x_k$ implies $a_i>a_k$ but $x_i\simeq x_k$ does not imply
$a_i=a_k$. 

%The next lemma says that the coefficients of an LPB representing a DNF
%must correspond to the order given by the occurrence patterns. 


%\begin{lemma}\label{DNF-occurrence-pattern-lem}
%Let $\phi$ be a DNF represented by the LPB $\coeffSum{1}{m}\geq d$. Then
%$a_i\geq a_k$ implies $\OP(\phi,x_i)\succeq\OP(\phi,x_k)$; moreover, there exists an LPB 
%$\coeffSumPrime{1}{m}\geq d'$ representing $\phi$ such that $\OP(\phi,x_i)=\OP(\phi,x_k)$
%implies $a'_i=a'_k$. 
%\end{lemma}

%\addtocounter{theorem}{1}%TR230

%%Occurrence patterns capture how replacing one
%%variable in a  clause of $\phi$ yields or does not yield another
%% clause of
%%$\phi$. In Ex.~\ref{op-ex}, $\OP(\phi,x_1)\succ\OP(\phi,x_2)$ reflects
%%that replacing $x_1$ by $x_2$ does not always yield a  clause of
%%$\phi$. 

%The following is a corollary of Lemmas \ref{symmetric-possible-lem} and 
%\ref{DNF-occurrence-pattern-lem}.

%\begin{corollary}\label{OP-symmetric-coro}
%If the DNF $\phi$ is represented by an LPB $I$, then 
%%$\phi$ is also representable by an LPB such that 
%$x_i,x_k$ are symmetric in $\phi$ iff  $x_i,x_k$ have identical occurrence patterns.
%%iff $x_i,x_k$ have identical coefficients. 
%\end{corollary}


%\subsection{Decomposing a DNF}\label{decomposition-subsec}
Suppose we want to find an LPB
representing $\phi$, and we have already established  
the order of the
coefficients. Assume the numbering of the variables
is such $x_1\succeq\ldots\succeq x_m$. Consider now the
maximal set $X=\{x_1,\ldots,x_l\}$ such that $x_1\simeq\ldots\simeq x_l$. 
%simplified special case we have used at the end of the introduction. 
%If $X$ is not symmetric in $\phi$, then  $\phi$ cannot be represented by an LPB
%and we can stop. Otherwise, 
%SPACE REASONS
We partition $\phi$ according to how many
variables from $X$ each  clause contains. We then remove the variables
from $X$ from each clause, which gives $l+1$ subproblems. Theorem
\ref{DNF-encoding-generalisation-thm} states under which conditions 
solutions to these
subproblems can be combined to an LPB for $\phi$. %However, since the
%solutions have to be similar in a certain sense, it turns out that we
%cannot simply solve the subproblems independently and \emph{then}
%combine the solutions, but we must solve the subproblems in parallel,
%as will be shown in Subsec.~\ref{composition-subsec}.

%The following statements do not require $X$ to be \emph{maximal},
%e.g.~if $\{x_1,\ldots,x_5\}$ is the maximal set such that
%$x_1\simeq\ldots\simeq x_5$, then the statements will also hold for
%$X=\{x_1,x_2,x_3\}$. %From now on, the letter $X$ will always denote 
%%a set as just described, maximal or not.

%In the sequel, the letter $X$ will always represent a set
%as described in the previous paragraph, or (in particular in
%Subsec.~\ref{composition-subsec}) a subset thereof.

\begin{definition}\label{Cut-def}
Let $\phi$ be a DNF and $X$ a subset of its variables with $|X| =l$.
If $\phi$ contains a clause $c\subseteq X$, then let $k_{\max}$ be the length of
the longest such clause; otherwise let $k_{\max}:=\infty$. 
For $0\leq k\leq l$,  we define
$\Cut{\phi}{X}{k}$ as the disjunction of  clauses from $\phi$ 
containing exactly $\min\{k,k_{\max}\}$ variables from $X$, with those 
variables removed. 
\end{definition}

When constructing the $\Cut{\phi}{X}{k}$ from $\phi$, we say that we \emph{split away} 
the variables in $X$ from $\phi$. 

%It is easy to see that $\Cut{\phi}{X}{k}$ is the formula obtained from $\phi$ by
%making $k$ variables from 


\begin{example}\label{Cut-ex}
Let $\phi\equiv(x_1)\lor(x_2)\lor(x_3\land x_4)$ and $X=\{x_1,x_2\}$.
We have $k_{\max}=1$.
Then $\Cut{\phi}{X}{0}=(x_3\land x_4)$, 
$\Cut{\phi}{X}{1}=\true$ (i.e.~the disjunction of twice the 
empty conjunction), and 
$\Cut{\phi}{X}{2}=\true$.
\end{example}

We must solve the $l+1$ subproblems in such a way that the
resulting LPBs agree in all coefficients, and that the threshold difference of
neighbouring LPBs is always the same. Before giving the theorem,
we give two examples for illustration. 

\begin{example}\label{simplest-alg-ex}
Consider 
$\phi\equiv(x_1\land x_2)\lor(x_1\land x_3)\lor(x_1\land x_4)\lor(x_2\land x_3\land x_4)$ and $X=\{x_1\}$.
Then $\Cut{\phi}{X}{0}=x_2\land x_3\land x_4$, represented by $x_2+x_3+x_4\geq3$.
Moreover, $\Cut{\phi}{X}{1}=x_2\lor x_3\lor x_4$, represented by $x_2+x_3+x_4\geq1$.

Since the coefficients of the two LPBs agree, it turns out that $\phi$
can be represented by $2x_1+x_2+x_3+x_4\geq3$. The coefficient of $x_1$
is given by the difference of the two thresholds, i.e.~$3-1$.
\end{example}

\begin{example}\label{LPB-adaptation-ex}
Consider 
$\phi\equiv(x_1\land x_2)\lor(x_1\land x_3\land x_4)\lor(x_2\land x_3\land x_4)$ and
$X=\{x_1,x_2\}$. We have
$\Cut{\phi}{X}{0}=\false$, represented by $x_3+x_4\geq4$, 
$\Cut{\phi}{X}{1}=x_3\land x_4$, represented by $x_3+x_4\geq2$, and  
$\Cut{\phi}{X}{2}=\true$, represented by $x_3+x_4\geq0$. 
The DNF $\phi$ is represented by $2x_1+2x_2+x_3+x_4\geq4$. 
The coefficient of $x_1,x_2$ is given by $4-2=2-0=2$ 
(the thresholds are ``equidistant'').   
\end{example}


\begin{theorem}\label{DNF-encoding-generalisation-thm}
Let $\phi$ be a DNF in variables $x_1,\ldots,x_m$ and suppose 
$X=\{x_1,\ldots,x_l\}$ are symmetric variables that are maximal 
w.r.t.~$\succeq$ in $\phi$. Then $\phi$ is represented by an LPB 
$\coeffSum{1}{m}\geq d$, where $a_1=\ldots=a_l$, iff for all $k\in\zerotol$,
the DNF $\Cut{\phi}{X}{k}$ is represented by 
$\coeffSum{l+1}{m}\geq d-k\cdot a_1$. 

\addtocounter{equation}{1}%TR230
%\input{proofs_VMCAI07_submission/DNF-encoding-generalisation-thm}
\end{theorem}

Unfortunately, Thm.~\ref{DNF-encoding-generalisation-thm} does not immediately
dictate an algorithm for computing an LPB for a DNF if possible. 

The remaining problem is that a DNF might be represented by various LPBs, and so
even if the LPBs computed recursively do not have agreeing coefficients and
equidistant thresholds, one might find alternative LPBs 
(such as the non-obvious LPB for $\false$ in
Ex.~\ref{LPB-adaptation-ex}) so that
Thm.~\ref{DNF-encoding-generalisation-thm} can be applied.


%The unification problem can be divided into the problems of making the
%coefficients agree and making the thresholds equidistant. 
%We now present a solution to the second problem.

%Before addressing this problem, 
We now generalise LPBs by recording to what extent
thresholds can be shifted without changing the meaning. To formulate this, we
temporarily lift the restriction that coefficients and thresholds must be
integers. How to obtain integers in the end is explained at the end of
the section. 

\begin{definition}
Given an LPB $I\equiv \coeffSum{1}{m}\geq d$, we call 
$\mint$ the \defining{minimum threshold} of $I$ if 
$\mint$ is the smallest number (possibly $-\infty$) such that for any 
$\mint'\in (\mint,d]$,  the LPB
$\coeffSum{1}{m}\geq \mint'$ represents the same  function as $I$. 
We call $\maxt$ the \defining{maximum threshold} if $\maxt$ is the 
biggest number (possibly $\infty$) such that 
$\coeffSum{1}{m}\geq \maxt$ represents the same  function as $I$.
We call $\maxt-\mint$ the \defining{gap} of $I$. 
\end{definition}

Note that the minimum threshold of $I$ is not a possible threshold
of $I$. %the same LPB, and that it is at least smaller by 1 than any actual
%integer threshold. 
Since the minimum and maximum thresholds of an LPB are more
informative than its actual threshold, we use %in our algorithm 
the notation $\coeffSum{1}{m}\geq \threshold{\mint}{\maxt}$ for denoting an LPB with minimum
threshold $\mint$ and maximum threshold $\maxt$.


%The next lemma strengthens Thm.~\ref{DNF-encoding-generalisation-thm}, stating
%that information about minimum and maximum thresholds can be maintained with
%little overhead.


%\begin{lemma}\label{threshold-slack-lem}
%Make the same assumptions as in
%Thm.~\ref{DNF-encoding-generalisation-thm}, and assume that  
%for all $k\in\zerotol$, the DNF $\Cut{\phi}{X}{k}$ is represented by 
%$I^k\equiv \coeffSum{l+1}{m}\geq d-k\cdot a_1$. Moreover, for all
%$k\in\zerotol$, let $\mint_k,\maxt_k$ be minimum and maximum
%thresholds of $I^k$, respectively. Then
%%$\mint:=\mint_0+\max_{k\in\zerotol}(k\cdot a_1+\mint_k-\mint_0)$, 
%$\mint:=\max_{k\in\zerotol}(\mint_k+k\cdot a_1)$, 
%%$\maxt:=\maxt_0-\max_{k\in\zerotol}(\maxt_0-\maxt_k-k\cdot a_k)$ are the 
%$\maxt:=\min_{k\in\zerotol}(\maxt_k+k\cdot a_k)$ are the 
%minimum and maximum thresholds of $\coeffSum{1}{m}\geq d$. 
%\end{lemma}

%\addtocounter{equation}{1}

%\subsection{Composing LPBs}\label{composition-subsec}
Theorem \ref{DNF-encoding-generalisation-thm} suggests a recursive algorithm
where, at least conceptually, in the base case we have at most $2^{m}$ trivial
problems of determining an LPB%, trivial since the formula for which we must find
%an LPB is either $\true$ or $\false$
.


\begin{example}\label{op-cont-ex}\label{op-ex}
Consider $\phi\equiv(x_1\land x_2)\lor(x_1\land x_3)\lor(x_1\land x_4)\lor(x_1\land x_5)\lor(x_2\land x_3)\lor
(x_2\land x_4)\lor(x_3\land x_4\land x_5)$. 
To find an LPB for $\phi$, we must find LPBs for
$\Cut{\phi}{\{x_1\}}{0}$ 
and $\Cut{\phi}{\{x_1\}}{1}$.
To find an LPB for $\Cut{\phi}{\{x_1\}}{0}$, we must find LPBs for
$\Cut{\Cut{\phi}{\{x_1\}}{0}}{\{x_2\}}{0}$ and 
$\Cut{\Cut{\phi}{\{x_1\}}{0}}{\{x_2\}}{1}$, and so forth. Table \ref{op-cont-table} gives all 
the formulae for which we must find LPBs. 
For a concise notation we use some abbreviations which we explain using 
$\CutT{x_{3..5}}{0}\equiv f$ in the top-right corner: it stands for  
$\Cut{(x_3\land x_4\land x_5)}{\{x_3,x_4,x_5\}}{0}\equiv\false$, i.e.~the 
`$\cdot$' stands for the nearest \emph{non-shaded} formula to the left, here 
$(x_3\land x_4\land x_5)$. Note how we arranged the subproblem formulae in the table: 
e.g.~$(x_3\land x_4\land x_5)$ has \emph{three} symmetric variables that are split away to
obtain the subproblems to be solved, so these subproblems are located \emph{three}
columns to the right of $(x_3\land x_4\land x_5)$. The two shaded boxes in between contain the
subproblems obtained by splitting away only $\{x_3\}$, $\{x_3,x_4\}$, resp.
%Observe also the empty box in the last column, arising from the fact that we do
%not attempt to split away $x_5$ from $x_3\lor x_4$. 
\end{example}

\begin{table*}[t]
\begin{tabular}{l|l|l|l|l|l}
&                      &                      &                             & \ld{$\CutT{x_{3..4}}{0}\equiv f$} & $\CutT{x_{3..5}}{0}\equiv f$\\
&$\CutT{x_1}{0}$        & $\CutT{x_2}{0}\equiv$      &\sd{$\CutT{x_{3}}{0}\equiv f$}      & \ld{$\CutT{x_{3..4}}{1}\equiv f\quad\dagger$} & $\CutT{x_{3..5}}{1}\equiv f$ \\
&$\equiv(x_2\land x_3)\lor$         & $(x_3\land x_4\land x_5)$      & \sd{$\CutT{x_{3}}{1}$}         &  \ld{$\CutT{x_{3..4}}{2}\equiv x_5$} & $\CutT{x_{3..5}}{2}\equiv f$ \\
&$(x_2\land x_4)\lor$          &                      & \sd{$\equiv (x_4\land x_5)$}            &                         &  $\CutT{x_{3..5}}{3}\equiv t$\\\cline{4-6}
&$(x_3\land x_4\land x_5)$      & $\CutT{x_2}{1}\equiv$    & \ld{$\CutT{x_{3}}{0}\equiv x_4$}      & $\CutT{x_{3..4}}{0}\equiv f$ & \\
&                     &    $x_3\lor x_4$         & \ld{$\CutT{x_{3}}{1}\equiv t$}       & $\CutT{x_{3..4}}{1}\equiv t$ & \\
\raisebox{-1ex}[0cm][0cm]{$\phi$}&     &     &                                 & $\CutT{x_{3..4}}{2}\equiv t$ & \\\cline{3-6}
&&&&&\\[-2.7ex]                   
&                     &                    & \sd{$\CutT{x_{2..3}}{0}\equiv$}         & \ld{$\CutT{x_{2..4}}{0}\equiv x_5$} &$\CutT{x_{2..5}}{0}\equiv f$ \\
&$\CutT{x_1}{1}$       &\ud{$\CutT{x_2}{0}\equiv$}& \sd{$x_4\lor x_5$}               & \ld{$\CutT{x_{2..4}}{1}\equiv t$} &$\CutT{x_{2..5}}{1}\equiv t$ \\
&$\equiv x_2\lor x_3$            &\ud{$x_3\lor x_4\lor x_5$}     & \sd{$\CutT{x_{2..3}}{1}\equiv t$}       & \ld{$\CutT{x_{2..4}}{2}\equiv t$} &$\CutT{x_{2..5}}{2}\equiv t$ \\
&$\lor x_4\lor x_5$            &\ud{$\CutT{x_2}{1}\equiv t$}& \sd{$\CutT{x_{2..3}}{2}\equiv t$}        & \ld{$\CutT{x_{2..4}}{3}\equiv t$} & $\CutT{x_{2..5}}{3}\equiv t$\\
&                     &                   &                                &                    &$\CutT{x_{2..5}}{4}\equiv t$
\vspace{1ex}
\end{tabular}\caption{The recursive problems of Ex.~\ref{op-cont-ex}\label{op-cont-table}}
\end{table*}

%It turns out that we can solve the unification problem by not regarding it as a
%problem separate from the recursive procedure, but rather by weaving the
%unification into the way the results of the recursive calls are combined. 
The algorithm we propose is not a purely recursive one, since the subproblems
at each level must be solved in parallel. 
Explained using the example, we first find LPBs for the
formulae in the rightmost column, which have $0$ variables and hence we must
determine $0$ coefficients. Next to the left, we have formulae that contain (at
most) $x_5$, and we determine LPBs representing these, where we use the same
$a_5$ for all formulae! Then we determine $a_4$, and so forth. 


Taking $(x_3\land x_4\land x_5)$ in Table \ref{op-cont-table} as an example,
Thm.~\ref{DNF-encoding-generalisation-thm} suggests that $a_3,a_4,a_5$ should be
equal ($x_3,x_4,x_5$ are symmetric) and determined in one go.  However,
since $x_3,x_4,x_5$ are not globally symmetric, one cannot determine $a_3,a_4,a_5$
in one go, but rather first $a_5$, then $a_4$, then $a_3$. Therefore, it is
necessary to consider the formulae obtained by splitting away just
$x_3$ and then $x_4$. These are the shaded formulae.

We call the formulae in column $l+1$ the $l$-\emph{successors}. Shaded formulae are
called \emph{auxiliary}, the others are called \emph{main}. Formulae that have
no further formulae to the right are called \emph{final}. 

\begin{definition}\label{successor-def}
Let $\phi$ be a DNF in $m$ variables. Then $\phi$ is the $0$-\defining{successor} of
$\phi$. Furthermore, $\phi$ is a \defining{main} successor of $\phi$. 
Moreover, if $\phi'$ is a main $n$-successor of $\phi$, and $l$ is maximal 
so that $x_{n+1},\ldots,x_{n+l}$ are  symmetric in
$\phi'$, then for all $l', k$ with $1\leq l'\leq l$ and 
$0\leq k\leq l'$, we say that $\Cut{\phi'}{\{x_{n+1},\ldots,x_{n+l'}\}}{k}$ is an $(n+l')$-successor of
$\phi$. The  $(n+l)$-successors are called \defining{main}, and for $l'<l$, the 
$(n+l')$-successors are called \defining{auxiliary}. 
%If $x_{n+1},\ldots,x_{n+l}$ are the only variables of $\phi'$, then we call the
%$(n+l)$-successors \defining{final}.
%Wenzelmann discovers on 25.7.11:
A node that is a main node and $\true$ or $\false$ is 
called \emph{final}. 
\end{definition}

Note in particular $x_3\lor x_4$ in column 3 in Table \ref{op-cont-table}. It does
not contain $x_5$, and so we obtain final $4$-successors in the
last-\emph{but-one} column. Clearly, a final successor of $\phi$ is either $\true$
or $\false$.

Generally, each non-final successor is associated with two formulae in the 
column right next to it, one shifted up and one down, obtained by 
splitting away the variable with the smallest index. 
In fact, Table \ref{op-cont-table} resembles a binary tree with the
root displayed to the left. However, it is \emph{not quite} a tree: take
the node $x_4\land x_5$ and the node $f$ above it, for instance; the 
``upper child'' of  $x_4\land x_5$ and the ``lower child'' of $f$
coincide; they are both the $f$-node marked with $\dagger$. 

The following proposition explains this sharing.

\begin{proposition}\label{split-away-fewer-prop}
Assume $\phi$, $\phi'$, $n$, $l$ as in Def.~\ref{successor-def}. For  
$0< l'<l$ and $0\leq k\leq l'$, we have 
\[
\begin{array}{l}
\Cut{\Cut{\phi'}{\{x_{n+1},\ldots,x_{n+l'}\}}{k}}{\{x_{n+l'+1}\}}{0}\equiv\\
\qquad \Cut{\phi'}{\{x_{n+1},\ldots,x_{n+l'+1}\}}{k}\\
\Cut{\Cut{\phi'}{\{x_{n+1},\ldots,x_{n+l'}\}}{k}}{\{x_{n+l'+1}\}}{1}\equiv\\
\qquad \Cut{\phi'}{\{x_{n+1},\ldots,x_{n+l'+1}\}}{k+1}
\end{array}
\]
\end{proposition}

Taking $\phi'\equiv x_3\land x_4\land x_5$, e.g., the proposition says that 
$\Cut{\Cut{\phi'}{\{x_3\}}{0}}{\{x_4\}}{1}$
and
$\Cut{\Cut{\phi'}{\{x_3\}}{1}}{\{x_4\}}{0}$ 
are both equal to $\Cut{\phi'}{\{x_3,x_4\}}{1}\equiv \false$.  

If we took a naïve approach where we always
split away one variable at a time, we would have a table (tree) 
with $32$ ($=2^m$) formulae in the rightmost column. Thanks to the
sharing, we only have 12 final formulae instead.
\label{only12}

%TODO: evaluate this in general. 
Note that the initial work by Coates and Lewis \cite{CoaLew61}
indeed corresponds to the naïve approach, except that nodes containing
$\true$ or $\false$ are not expanded further. 
Coates et al.~\cite{CoaKirLew62} have improved this method by
considering symmetries, but only ``global'' symmetries that are present in the
initial DNF $\phi$, not ``local'' symmetries that appear only after splitting. Even
for initial DNFs without any global symmetries, many local symmetries
usually appear after splitting. 

%It seems to be generally the case that the table has much fewer final
%nodes that $2^m$.  The many examples we looked at strongly suggest
%that even if one tries to construct an input DNF that has as few
%symmetries as possible and hence would lead to a big table, the
%subformulae constructed by the splitting always exhibit many
%symmetries. It would be interesting to have a theoretical statement
%about this observation. 


%Our aim is to show how, given LPB representations of all the formulae in column
%$k$, all using the same coefficients $a_k,\ldots a_m$, we can derive LPB
%representations of all the formulae in column $k-1$, all using the same
%coefficients $a_{k-1},\ldots a_m$. Since column $1$ contains just $\phi$, once we arrive
%at $k=1$ we have solved our problem.

%The following lemma says under which conditions it is possible to find an
%agreeing coefficient for the next step, and how it is done.

The following theorem states if and how one can find the next coefficient and
thresholds for representing all $k$-successors of $\phi$ provided one has
coefficients and thresholds for representing all $(k+1)$-successors.


\begin{theorem}\label{ak-completion-criterion-thm}
Assume $\phi$ as in Thm.~\ref{DNF-encoding-generalisation-thm} and some $k$ with 
$0\leq k\leq m-1$, and let $\Phi_k$ be the set of $k$-successors of $\phi$.
For every non-final $\phi'\in\Phi_k$, suppose we have two LPBs
$\coeffSum{k+2}{m}\geq\threshold{\mint_{\phi'0}}{\maxt_{\phi'0}}$ and 
$\coeffSum{k+2}{m}\geq\threshold{\mint_{\phi'1}}{\maxt_{\phi'1}}$, representing $\Cut{\phi'}{\{x_{k+1}\}}{0}$ and
$\Cut{\phi'}{\{x_{k+1}\}}{1}$, respectively. 

If it is possible to choose $a_{k+1}$ such that 
\begin{equation}\label{maxmin-diff-eq}
\max_{\phi'\in\Phi_k} (\mint_{\phi'0}-\maxt_{\phi'1}) < a_{k+1}< \min_{\phi'\in\Phi_k} (\maxt_{\phi'0}-\mint_{\phi'1}),
\end{equation}
then for all $\phi'\in\Phi_k$, the LPB $\coeffSum{k+1}{m}\geq\threshold{\mint_{\phi'}}{\maxt_{\phi'}}$ represents
$\phi'$, where %we define
%\begin{equation}\label{new-minmax-eq}
%\mint_{\phi'}=\max\{\mint_{\phi'0},\mint_{\phi'1}+a_{k+1}\} \ \mbox{and}\ 
%\maxt_\phi'=\min\{\maxt_{\phi'0},\maxt_{\phi'1}+a_{k+1}\} 
%\end{equation}
\begin{gather}
\!\!
\mint_{\phi'}=\max\{\mint_{\phi'0},\mint_{\phi'1}+a_{k+1}\},\; 
\maxt_{\phi'}=\min\{\maxt_{\phi'0},\maxt_{\phi'1}+a_{k+1}\}\notag \\ \mbox{for non-final $\phi'$}\label{new-minmax-eq}\\
\!\!
\mint_{\phi'}=-\infty,\;\maxt_{\phi'}=0 \ \mbox{for $\phi'\equiv\true$},\ 
\mint_{\phi'}={\textstyle\sum_{i=k+1}^m}a_i,\;\maxt_{\phi'}=\infty\notag  \\ \mbox{for $\phi'\equiv\false$}\label{new-minmax-2-eq}
\end{gather}
%TODO: cannot stay like this. 
%If such an $a_{k+1}$ cannot be chosen, 
If $\max_{\phi'\in\Phi_k} (\mint_{\phi'0}-\maxt_{\phi'1}) \geq \min_{\phi'\in\Phi_k} (\maxt_{\phi'0}-\mint_{\phi'1})$, 
then no $a_{k+1}$, $\mint_{\phi'}$,
$\maxt_{\phi'}$ exist such that 
$\coeffSum{k+1}{m}\geq\threshold{\mint_{\phi'}}{\maxt_{\phi'}}$ represents $\phi'$ for all $\phi'\in\Phi_k$.

%\input{proofs_CPAIOR07_submission/ak-completion-criterion-thm}
\end{theorem}

Following \cite{CoaLew61}, we call the interval for $a_{k+1}$ given
by (\ref{maxmin-diff-eq}) the \defining{range} of $a_{k+1}$. 

The $m$-successors of $\phi$ are represented by LPBs with an empty sum as
l.h.s.: $\sum_{i=m+1}^ma_ix_i\geq\threshold{0}{\infty}$ for $\false$,
$\sum_{i=m+1}^ma_ix_i\geq\threshold{-\infty}{0}$ for $\true$. Then we proceed using
Thm.~\ref{ak-completion-criterion-thm}, in each step choosing an
arbitrary $a_{k+1}$ fulfilling (\ref{maxmin-diff-eq}).


\begin{table*}[t]
\begin{center}
\begin{tabular}{r|r|r|r|r|r}
%$4x_1+3x_2+$&&&&&\\
%$2x_3+2x_4+$&$3x_2+2x_3$    & $2x_3+$               &                             &                          &  \\
%$x_5\geq\ldots$& $2x_4+x_5\geq\ldots$ & $2x_4+x_5\geq\ldots$             & $2x_4+x_5\geq\ldots$                & $x_5\geq\ldots$                   & $\sum_{i=6}^5a_ix_i\geq\ldots$\\\hline\hline  
$4x_1+3x_2+$&     $3x_2+$  &                      &                          &                    &              \\
$2x_3+2x_4+$&$2x_3+2x_4+$  & $2x_3+2x_4+$            &        $2x_4+$            &                      & $\sum_{i=6}^5a_ix_i$ \\
$x_5\geq\ldots$&$x_5\geq\ldots$        & $x_5\geq\ldots$               &  $x_5\geq\ldots$               &   $x_5\geq\ldots$             &  $\geq\ldots$    \\\hline\hline
&                      &                      &                             & \ld{$\LPBT{x_{3..4}}{0}\threshold{1}{\infty}$} & $\LPBT{x_{3..5}}{0}\threshold{0}{\infty}$\\
&$\LPBT{x_1}{0}$        & $\LPBT{x_2}{0}$      & \sd{$\LPBT{x_{3}}{0}\threshold{3}{\infty}$}     & \ld{$\LPBT{x_{3..4}}{1}\threshold{1}{\infty}$} & $\LPBT{x_{3..5}}{1}\threshold{0}{\infty}$ \\
&                     & \ub{$\threshold{4}{5}$}         & \sd{$\LPBT{x_{3}}{1}\threshold{2}{3}$}      &  \ld{$\LPBT{x_{3..4}}{2}\threshold{0}{1}$} & $\LPBT{x_{3..5}}{2}\threshold{0}{\infty}$ \\
&$\threshold{4}{5}$              &                      &                                 &                         &  $\LPBT{x_{3..5}}{3}\threshold{-\infty}{0}$\\\cline{4-6}
&                     & $\LPBT{x_2}{1}$    & \ld{$\LPBT{x_{3}}{0}\threshold{1}{2}$}      & $\LPBT{x_{3..4}}{0}\threshold{1}{\infty}$ & \\
&                     &    $\threshold{1}{2}$         & \ld{$\LPBT{x_{3}}{1}\threshold{-\infty}{0}$}       & $\LPBT{x_{3..4}}{1}\threshold{-\infty}{0}$ & \\
\raisebox{-1ex}[0cm][0cm]{$\threshold{4}{5}$}&     &     &                                 & $\LPBT{x_{3..4}}{2}\threshold{-\infty}{0}$ & \\\cline{3-6}
&&&&&\\[-2.7ex]                   
&                     &                    &                                 & \ld{$\LPBT{x_{3..4}}{0}\threshold{0}{1}$} &$\LPBT{x_{3..5}}{0}\threshold{0}{\infty}$ \\
&$\LPBT{x_1}{1}$       &                    &\sd{$\LPBT{x_{3}}{0}\threshold{0}{1}$}      & \ld{$\LPBT{x_{3..4}}{1}\threshold{-\infty}{0}$} &$\LPBT{x_{3..5}}{1}\threshold{-\infty}{0}$ \\
&$\threshold{0}{1}$              &\ud{$\LPBT{x_2}{0}\threshold{0}{1}$}& \sd{$\LPBT{x_{3}}{1}\threshold{-\infty}{0}$}       & \ld{$\LPBT{x_{3..4}}{2}\threshold{-\infty}{0}$} &$\LPBT{x_{3..5}}{2}\threshold{-\infty}{0}$ \\
&                     &\ud{$\LPBT{x_2}{1}\threshold{-\infty}{0}$}& \sd{$\LPBT{x_{3}}{2}\threshold{-\infty}{0}$}   & \ld{$\LPBT{x_{3..4}}{3}\threshold{-\infty}{0}$} & $\LPBT{x_{3..5}}{3}\threshold{-\infty}{0}$\\
&                     &                   &                                &                    &$\LPBT{x_{3..5}}{4}\threshold{-\infty}{0}$
\end{tabular}
\end{center}
\vspace{1ex}
\caption{LPBs for Ex.~\ref{op-cont-ex}\label{op-cont-thresh-table}}
\end{table*}


\begin{example}
Consider again Ex.~\ref{op-cont-ex}. Table
\ref{op-cont-thresh-table} is arranged in strict correspondence to Table
\ref{op-cont-table} and shows LPBs for all successors of $\Phi$. 
In the top line we give the l.h.s.~of the LPBs, which is of
course the same for each LPB in a column.
In the main table, we list the minimum and maximum threshold of each formula. 
%Unfortunately, space
%restrictions force us to give only the minimum and maximum thresholds for each
%formula and not the formula itself, which has to be looked up by matching the
%two tables. On the other hand, this underlines the fact that once we have filled
%out the rightmost column, computing the coefficients and thresholds just
%``mechanically'' follows certain rules. 


In the first step, applying (\ref{maxmin-diff-eq}), we have to choose $a_5$
so that
\[
\begin{array}{l}
\max\{0-\infty,0-\infty,0-0,\quad 0-0,-\infty-0,-\infty-0,-\infty-0\}<a_5<\\
\min\{\infty-0,\infty-0,\infty--\infty,\quad \infty--\infty,0--\infty,0--\infty,0--\infty\}.
\end{array}
\]  
Choosing $a_5=1$ will do. The minimum and maximum thresholds in column 5
are computed using (\ref{new-minmax-eq}); e.g.~the topmost $\threshold{1}{\infty}$ is 
$\threshold{\max\{0,0+1\}}{\min\{\infty,\infty+1\}}$. 

In the next step, we have to choose $a_4$ so that 
 \[
\begin{array}{l}
\max\{1-\infty,1-1,\quad 1-0,-\infty-0, \quad 0-0,-\infty-0,-\infty-0\}<a_4<\\
\min\{\infty-1,\infty-0,\quad \infty--\infty,0--\infty,\quad 1--\infty,0--\infty,0--\infty\}.
\end{array}
\]  
Choosing $a_4=2$ will do. Note that the bound $1-0<a_4$ comes from the
middle box of the fifth column and thus ultimately from $x_3\lor x_4$. Our
algorithm enforces that $a_4>a_5$, which must hold for an LPB representing 
$x_3\lor x_4$.

In the next step, $a_3$ can also be
chosen to be any number $>1$ so we choose $2$ again.\footnote{The algorithm
  could be improved by determining $a_3$ and $a_4$ in one go since $x_3,x_4$ are
symmetric in $\phi$. We refrain from spelling this out to avoid
further complication.} 
In the next step, $2<a_2<4$
must hold so we choose $a_2=3$. Finally, $3<a_1<5$ must hold so we choose
$a_1=4$. We obtain the LPB $4x_1+3x_2+2x_3+2x_4+x_5\geq\threshold{4}{5}$ given in Ex.~\ref{op-ex}.
\end{example}


We have seen in the example how our algorithm works. However, since the choice
of $a_{k+1}$ is not unique in general, %one might be worried that 
a bad choice
of $a_{k+1}$ might later lead to non-applicability of
Thm.~\ref{ak-completion-criterion-thm}. %We have a lemma stating that this is not
%a problem \cite{SmaTR230-07nociteother}.
%(Lemma \ref{coeff-intersect-lem}).
%TR230
% Wenzelmann:
%Contrary to what was stated by Smaus \shortcite{SmaTR230-07nociteother},
%this is indeed a problem. We have suggested
%to choose $a_{k+1}$ always as the smallest possible integer value to obtain an LPB
%with small coefficients.
%But it turns out that this strategy sometimes leads to a dead end.
%
For example, 
%\begin{example}\label{incompleteness-example}
consider the DNF
\begin{align*}
\phi \equiv \left( x_1 \land x_2 \right) \lor \left( x_1 \land x_3 \right) \lor \left(x_1 \land x_4 \land x_5\right) \left(x_2 \land x_3 \land x_4\right)\\
\lor \left(x_2 \land x_3 \land x_5 \right) \lor \left( x_2 \land x_4 \land x_5 \right) \lor \left( x_3 \land x_4 \land x_5 \land x_6 \right)
\end{align*}
Applying the strategy of choosing $a_{k+1}$ always as the smallest
possible integer value, the algorithm runs into a dead end. 

% TODO: vielleicht auch die ganzen Nachfolger angeben? Aber Tabelle ist sehr gro??...
%We apply the algorithm to create all successors of $\phi$ and calculate
%LPBs for all recursive subproblems. The corresponding LPBs can be
%found in Table \ref{table-incompleteness-solutions}. By applying the
%strategy of choosing the coefficient as small as possible we choose 
%$a_6 = 1, a_5=2, a_4 = 2$. We use the minimum and maximum degrees in
%the fourth column to choose the coefficient $a_3$. We have to choose $a_3$ s.\,t.
%\begin{align*}
%&\max\left\lbrace 5-5,\, 3-2\,, 3-0,\, -\infty - 0 \right\rbrace < a_3 <\\
%&\min\left\lbrace \infty - 4,\, 4-1,\, 4 -- \infty,\, 0 -- \infty \right\rbrace
%\end{align*}
%i.\,e. $3 < a_3 < 3$. This is, of course, not possible. But $\phi$ can be represented by the LPB $9x_1 + 7x_2 + 6x_3 + 4x_4 + 4x_5 + x_6 \geq 15$.

%The algorithm found solutions for all subproblems in the fourth
%column. 
%But we cannot combine the coefficients chosen so far to a solution representing all LPBs in the third column.

%Alternatively, we were allowed to choose $a_5 = a_4 = 4$, and if we do so, we obtain an appropriate LPB. Therefore the applicability of Thm.~\ref{ak-completion-criterion-thm} depends on the choice of the previous coefficients.
%\end{example}


%TODO: Discuss choices, which are not, we now know, just "pragmatic". 
%However, there are some pragmatic choices.  As stated in the example, to obtain
%an LPB with small coefficients, one might always choose $a_{k+1}$ as the smallest
%possible integer value. 

Another problem seems to be that $a_{k+1}$ could be forced to be
between neighbouring integers, in which case it cannot be an integer
itself. However, 
in this case, one can multiply all LPBs of the current system
by 2 (this obviously preserves the meaning of the LPBs) before
proceeding so that $a_{k+1}$ can be chosen to be an integer.

From the construction of the successors it follows that all formulae
in a column together have size less than all formulae in the column to
the left of it, so that the entire table has size less than $|\phi|\cdot
(m+1)$. One can thus show that the complexity of the algorithm is
polynomial in the size of $\phi$, while the size of $\phi$ itself can be
exponential in $m$.  


%\newpage

%\mbox{}

%\newpage



%\subsection{Completion according to \cite{CoaLew61}}
Concerning completeness, Coates and Lewis propose a backtracking 
based on identifying the nodes in the splitting tree that are
responsible for a conflict between constraints \cite{CoaLew61}. 
For space reasons, we
cannot explain here how this works, but our implementation takes it
into account. 


\section{Generating Random LPBs}
\label{random-sec}
In order to evaluate algorithms for the threshold recognition problem,
one needs benchmark DNFs. In \cite{PalGopTra10}, all monotone (unate)
Boolean functions of up to 5 variables are considered as input. For 6
variables, 200,000 ``random'' monotone functions are chosen as input.
However, we believe that for testing purposes, it is better to use DNFs
for which it is \emph{known} that they are threshold functions. To do
so, one should generate LPBs, convert them into DNFs, and then apply
the algorithms to those generated DNFs, hoping that the algorithm will
recognise them as threshold functions.

Apart from a few tests on non-threshold functions, we tested all
algorithms by generating LPBs where the coefficients are all positive
and non-increasing from $a_1$ to $a_m$. Up to $m=7$, we generated all 
%TODO: true???
LPBs up to equivalence. For bigger $m$, the number of LPBs becomes too
big and so we generated a ``random'' sample of LPBs.

For space reasons, we cannot describe our method in detail here, but
it was guided by the following principles: 
(1) the method should be simple and avoid ad-hoc choices; 
(2) it should be possible to calibrate how big the increase from the
smallest to the biggest coefficient is;  
(3) every coefficient vector (for given $m$) should have a positive
probability, however small, of being generated. 

%TODO: how many DNFs of how many variables did we eventually generate?

\section{Implementation}\label{impl-sec}
Both algorithms have been implemented in Java. They share the same core classes representing the main components such as DNFs and LPBs. The linear program is solved by \verb|lp_solve|.
Both implementations can be accessed and tested via a graphical user interface.

For testing the implementation we generated a full enumeration of LPBs up to seven variables. For LPBs with more variables we tested 180,000 randomly generated LPBs (with 8 to 25 variables). We transformed the LPBs to DNFs (so we know that for these DNFs there exists an LPB) to test the implementations. As expected the linear programming algorithm solved all tested input DNFs.

The combinatorial algorithm was able to solve all input DNFs with five or less variables. But it fails on some DNFs with six variables (with the strategy to choose $a_{k+1}$ as small as possible). Our empirical analysis shows that the more variables a DNF contains the more often the conversion fails. Circa 8\% of the tested DNFs with seven variables cannot be converted, for DNFs with 25 variables circa 86\% cannot be converted. The failure rate for 13 to 25 variables is illustrated in Figure \ref{fig:failure}.

%\begin{center}
\begin{figure}
\includegraphics[scale=1]{failure_diagram.pdf}
\caption{Failure rate of the combinatorial algorithm}
\label{fig:failure}
\end{figure}
%\end{center}

The linear programming algorithm was faster in direct runtime
comparison, but we're still working on improvements for the
combinatorial algorithm.

As discussed in Sec.~\ref{only12}, for the combinatorial algorithm
the number of \emph{final nodes} is an important criterion for its
theoretical runtime.  We plan to investigate this systematically in
the future, but to give some idea: for 25 variables, we had around 600
final nodes on average, while $2^{25}=33554432$.

%Figure \ref{fig:final} gives a first impression. 
%For all tested DNFs the average final node
%count for DNFs with $m$ variables was smaller than $m^2$.

%\begin{figure*}
%\begin{center}
%\includegraphics[scale=1]{runtime_graph.pdf}
%\caption{$\lambda(m)$ is the average number of final nodes for DNFs with $m$ variables.}
%\label{fig:final}
%\end{center}
%\end{figure*}


\section{Conclusion}\label{concl-sec}


%Hooker has proposed an algorithm for generating the strongest 0-1 ILP
%constraints, within a candidate set $T$, that are implied by a set $S$
%of 0-1 ILP constraints \cite{Hoo92}. Letting $T$ be the set of all
%LPBs, the algorithm can be used to transform a CNF to an LPB. However,
%the algorithm is practical only for certain restrictions of $T$. In
%the general case, which we need here, it is unclear if the algorithm
%is any better than enumerating and checking all LPBs. This is however
%an interesting topic for future work.

%TODO: clean up. I postpone this because PalGopTra10 should not just
%be mentioned here, but in several places in the paper. 
A method for solving the threshold recognition problem has been
presented recently at this very venue \cite{PalGopTra10}. The paper uses the
\emph{Chow parameters} \cite{CraHam11} of each variable as basis for deciding the
coefficient. We plan to investigate similar ideas, but only to provide
the Coates and Lewis algorithm %, which is theoretically well-understood,
with some \emph{heuristic value} for each coefficient, hoping that
this will reduce the need for backtracking. In contrast, the rationale
or theoretical foundation for the coefficient choices in
\cite{PalGopTra10} remain unclear to us. 
 
The method of \cite{PalGopTra10} is not complete. For 6 variables, the
method identifies around 70\% of the threshold functions. Contrast this
to Fig.~\ref{fig:failure}, showing that our implementation of the
Coates and Lewis algorithm without backtracking will have the same success
rate for around 13 variables.  

Beyond 6 variables, no statement is
possible because it is not known which of the used benchmarks are
threshold functions: the authors base their experiments on randomly
generated monotone functions. They do find 36 10-variable threshold
functions, however.

As Coates and Lewis stated in 1961 \cite{CoaLew61}, problems of this
size can still be solved by hand: 30 minutes for a 6-variable
function, 4 hours for a 12-variable function. 

As a future work, we want to use ideas from \cite{CoaKirLew62} to
choose each coefficient so that it maximises the gap of the subsequent
LPBs, which will hopefully reduce the need for backtracking. 

%\cite{CraHam11} shows that for many phenomena in Boolean functions, we
%need at least 9 or 10 variables to expose an example. 


\paragraph{Acknowledgements} 





%
% The following two commands are all you need in the
% initial runs of your .tex file to
% produce the bibliography for the citations in your paper.
\bibliography{smaus,own_publications}  % sigproc.bib is the name of the Bibliography in this case
% You must have a proper ".bib" file
%  and remember to run:
% latex bibtex latex latex
% to resolve all references
%
% ACM needs 'a single self-contained file'!
%
%APPENDICES are optional
%\balancecolumns

%\appendix
%Appendix A
%\balancecolumns % GM June 2007
% That's all folks!
\end{document}



%%% Local Variables:
%%% mode: latex
%%% x-symbol-8bits: t
%%% TeX-master: t
%%% coding: utf-8-unix
%%% End:
